[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification awbuf-inv
enrich
   error-class
, 
   avolume
, 
   nat-div
, 
   eraseblock
, 
   bufleb
with
   

   
   
   functions  . .align↓ : buffer → buffer;
              . .align↓ : avolume → avolume;
   predicates  awbuf-inv : avolume × bufleb;
               . ↓ . : avolume × avolume;
               . ↓ . : aleb × aleb;
               synced : avolume;
   
   
   
   

   

   axioms awbuf-inv-def
          : ⊦   awbuf-inv(avol, bleb)
              ↔ ¬
                ¬
                (  (∀ n. 
                        n < # avol ∧ avol[n].mapped?
                      → # avol[n].data ≤ LEB_SIZE ∧ (buffered(n) ≠ bleb → is-aligned(# avol[n].data, EB_PAGE_SIZE)))
                 ∧ (bleb ≠ nobuffer → bleb.leb < # avol ∧ avol[bleb.leb].mapped?));
          used for: ls;
          down-arrow-def :  ⊦ avol1 ↓ avol0 ↔ # avol1 = # avol0 ∧ (∀ n. n < # avol0 → avol1[n] ↓ avol0[n]);
          used for: ls;
          down-arrow-block-def
          : ⊦   aleb1 ↓ aleb0
              ↔   (aleb0.mapped? → aleb1 = mapped(aleb0.data.align↓))
                ∧ (¬ aleb0.mapped? ∧ aleb1.mapped? → # aleb1.data ≤ LEB_SIZE ∧ is-aligned(# aleb1.data, EB_PAGE_SIZE));
          used for: ls;
          down-arrow-buf :  ⊦ buf.align↓ = subarray(buf, 0, align↓(# buf, EB_PAGE_SIZE));
          used for: ls;
          down-arrow-size :  ⊦ # avol.align↓ = # avol;
          used for: s, ls;
          down-arrow-store-at :  ⊦ n < # avol → avol.align↓[n] = (avol[n].mapped? ⊃ mapped(avol[n].data.align↓);unmapped);
          used for: s, ls;
          synced :  ⊦ synced(avol) ↔ (∀ n. n < # avol ∧ avol[n].mapped? → is-aligned(# avol[n].data, EB_PAGE_SIZE));
          used for: ls;

   

   
end enrich